1  /-
  2  Copyright (c) 2019 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau
  5  
  6  Adjoining elements to form subalgebras.
  7  -/
  8  
  9  import ring_theory.algebra_operations ring_theory.polynomial ring_theory.principal_ideal_domain
src         └────────────────────────────┘ └────────────────────┘ └────────────────────────────────┘
 10  import algebra.pointwise
src         └───────────────┘
 11  
 12  universes u v w
 13  
 14  open lattice submodule ring
 15  
 16  namespace algebra
 17  
 18  variables {R : Type u} {A : Type v}
 19  variables [comm_ring R] [comm_ring A]
 20  variables [algebra R A] {s t : set A}
id                                  └─┘
src                                 └─┘
typ                                 └─┘
 21  
 22  theorem subset_adjoin : s ⊆ adjoin R s :=
 23  set.subset.trans (set.subset_union_right _ _) subset_closure
 24  
 25  theorem adjoin_le {S : subalgebra R A} (H : s ⊆ S) : adjoin R s ≤ S :=
 26  closure_subset $ set.union_subset S.3 H
 27  
 28  theorem adjoin_le_iff {S : subalgebra R A} : adjoin R s ≤ S ↔ s ⊆ S:=
 29  ⟨set.subset.trans subset_adjoin, adjoin_le⟩
 30  
 31  theorem adjoin_mono (H : s ⊆ t) : adjoin R s ≤ adjoin R t :=
 32  closure_subset (set.subset.trans (set.union_subset_union_right _ H) subset_closure)
 33  
 34  variables (R A)
 35  @[simp] theorem adjoin_empty : adjoin R (∅ : set A) = ⊥ :=
doc    └──┘
 36  eq_bot_iff.2 $ adjoin_le $ set.empty_subset _
 37  variables {A}
 38  
 39  variables (s t)
 40  theorem adjoin_union : adjoin R (s ∪ t) = (adjoin R s).under (adjoin (adjoin R s) t) :=
 41  le_antisymm
 42    (closure_mono $ set.union_subset
 43      (set.range_subset_iff.2 $ λ r, or.inl ⟨algebra_map (adjoin R s) r, rfl⟩)
 44      (set.union_subset_union_left _ $ λ x hxs, ⟨⟨_, subset_adjoin hxs⟩, rfl⟩))
 45    (closure_subset $ set.union_subset
 46      (set.range_subset_iff.2 $ λ x, adjoin_mono (set.subset_union_left _ _) x.2)
 47      (set.subset.trans (set.subset_union_right _ _) subset_adjoin))
 48  
 49  theorem adjoin_eq_span : (adjoin R s : submodule R A) = span R (monoid.closure s) :=
 50  begin
 51    apply le_antisymm,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
 52    { intros r hr, rcases ring.exists_list_of_mem_closure hr with ⟨L, HL, rfl⟩, clear hr,
src      └─────────┘  └─────┘                                 └────────────────┘  └──────┘
typ      └─────────┘  └─────┘                                 └────────────────┘  └──────┘
doc      └─────────┘  └─────┘                                 └────────────────┘  └──────┘
txt      └─────────┘  └─────┘                                 └────────────────┘  └──────┘
par      └─────────┘  └─────┘                                 └────────────────┘  └──────┘
pid            └───┘                                         └────────────────┘       └─┘
 53      induction L with hd tl ih, { rw mem_coe, exact zero_mem _ },
id                                                      └──────┘
src      └────────┘ └────────────┘    └─┘         └────┘└──────┘└─┘
typ      └────────┘ └────────────┘    └─┘         └────┘└──────┘└─┘
doc      └────────┘ └────────────┘    └─┘         └────┘        └─┘
txt      └────────┘ └────────────┘    └─┘         └────┘        └─┘
par      └────────┘ └────────────┘    └─┘         └────┘        └─┘
pid                └───────────┘                            └┘
st                                                └───────────────┘└┘
 54      rw list.forall_mem_cons at HL,
id          └──────────────────┘
src      └─┘└──────────────────┘└────┘
typ      └─┘└──────────────────┘└────┘
doc      └─┘                    └────┘
txt      └─┘                    └────┘
par      └─┘                    └────┘
pid                            └────┘
st   ────────────────────────────────┘└─
 55      rw [list.map_cons, list.sum_cons, mem_coe],
id           └───────────┘  └───────────┘  └─────┘
src      └──┘└───────────┘└┘└───────────┘└┘└─────┘
typ      └──┘└───────────┘└┘└───────────┘└┘└─────┘
doc      └──┘             └┘             └┘       
txt      └──┘             └┘             └┘       
par      └──┘             └┘             └┘       
pid        └┘             └┘             └┘       
st   ────────────────────┘└─────────────┘└───────┘└─
 56      refine submodule.add_mem _ _ (ih HL.2),
id              └───────────────┘      └┘ └┘
src      └─────┘└───────────────┘└───┘     └─┘
typ      └─────┘└───────────────┘└───┘ └┘└┘└─┘
doc      └─────┘                 └───┘     └─┘
txt      └─────┘                 └───┘     └─┘
par      └─────┘                 └───┘     └─┘
pid                             └───┘     └─┘
st   ─────────────────────────────────────────┘└─
 57      replace HL := HL.1, clear ih tl,
id                     └┘
src      └────────────┘  └┘  └─────────┘
typ      └────────────┘└┘└┘  └─────────┘
doc      └────────────┘  └┘  └─────────┘
txt      └────────────┘  └┘  └─────────┘
par      └────────────┘  └┘  └─────────┘
pid             └─┘└─┘  └┘       └────┘
st   ─────────────────────┘└───────────┘└─
 58      suffices : ∃ z r (hr : r ∈ monoid.closure s), has_scalar.smul.{u v} z r = list.prod hd,
id                                └────────────┘   └─────────────┘            └───────┘ └┘
src      └─────────┘└─────────┘ └────────────┘ └─────────────┘└─────┘  └───────┘
typ      └─────────┘└─────────┘ └────────────┘└─────────────┘└─────┘  └───────┘└┘
doc      └─────────┘ └─────────┘  └────────────┘                 └─────┘   └───────┘
txt      └─────────┘ └─────────┘                                 └─────┘            
par      └─────────┘ └─────────┘                                 └─────┘            
pid      └───────┘└┘ └─────────┘                                 └─────┘            
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
 59      { rcases this with ⟨z, r, hr, hzr⟩, rw ← hzr,
id                └──┘                            └─┘
src        └─────┘    └───────────────────┘  └───┘
typ        └─────┘└──┘└───────────────────┘  └───┘└─┘
doc        └─────┘    └───────────────────┘  └───┘
txt        └─────┘    └───────────────────┘  └───┘
par        └─────┘    └───────────────────┘  └───┘
pid                  └───────────────────┘    └─┘
st   ─────┘└──────────────────────────────┘└────────┘└─
 60        exact smul_mem _ _ (subset_span hr) },
id               └──────┘      └─────────┘ └┘
src        └────┘└──────┘└───┘ └─────────┘  └┘
typ        └────┘└──────┘└───┘ └─────────┘└┘└┘
doc        └────┘        └───┘              └┘
txt        └────┘        └───┘              └┘
par        └────┘        └───┘              └┘
pid                     └───┘              
st   ─────────────────────────────────────────┘└┘
 61      induction hd with hd tl ih, { exact ⟨1, 1, is_submonoid.one_mem _, one_smul _ _⟩ },
id                 └┘                               └──────────────────┘    └──────┘
src      └────────┘  └────────────┘    └────┘ └────┘└──────────────────┘└──┘└──────┘└────┘
typ      └────────┘└┘└────────────┘    └────┘ └────┘└──────────────────┘└──┘└──────┘└────┘
doc      └────────┘  └────────────┘    └────┘ └────┘                    └──┘        └────┘
txt      └────────┘  └────────────┘    └────┘ └────┘                    └──┘        └────┘
par      └────────┘  └────────────┘    └────┘ └────┘                    └──┘        └────┘
pid                 └───────────┘          └────┘                    └──┘        └───┘
st   ─────────────────────────────┘└──┘└─────────────────────────────────────────────────┘└┘
 62      rw list.forall_mem_cons at HL,
id          └──────────────────┘
src      └─┘└──────────────────┘└────┘
typ      └─┘└──────────────────┘└────┘
doc      └─┘                    └────┘
txt      └─┘                    └────┘
par      └─┘                    └────┘
pid                            └────┘
st   ────────────────────────────────┘└─
 63      rcases (ih HL.2) with ⟨z, r, hr, hzr⟩, rw [list.prod_cons, ← hzr],
id               └┘ └┘                              └────────────┘    └─┘
src      └─────┘     └──────────────────────┘  └──┘└────────────┘└──┘   
typ      └─────┘ └┘└┘└──────────────────────┘  └──┘└────────────┘└──┘└─┘
doc      └─────┘     └──────────────────────┘  └──┘              └──┘   
txt      └─────┘     └──────────────────────┘  └──┘              └──┘   
par      └─────┘     └──────────────────────┘  └──┘              └──┘   
pid                 └──────────────────────┘    └┘              └──┘   
st   ────────────────────────────────────────┘└──────────────────┘└─────┘└──
 64      rcases HL.1 with ⟨⟨hd, rfl⟩ | hs⟩ | rfl,
id              └┘
src      └─────┘  └────────────────────────────┘
typ      └─────┘└┘└────────────────────────────┘
doc      └─────┘  └────────────────────────────┘
txt      └─────┘  └────────────────────────────┘
par      └─────┘  └────────────────────────────┘
pid              └────────────────────────────┘
st   ──────────────────────────────────────────┘└─
 65      { refine ⟨hd * z, r, hr, _⟩, rw [smul_def, smul_def, map_mul, ring.mul_assoc], refl },
id                 └┘      └┘          └──────┘  └──────┘  └─────┘  └────────────┘
src        └─────┘    └┘ └┘  └──┘  └──┘└──────┘└┘└──────┘└┘└─────┘└┘└────────────┘  └───┘
typ        └─────┘ └┘└┘└┘└┘└──┘  └──┘└──────┘└┘└──────┘└┘└─────┘└┘└────────────┘  └───┘
doc        └─────┘     └┘ └┘  └──┘  └──┘        └┘        └┘       └┘                └───┘
txt        └─────┘     └┘ └┘  └──┘  └──┘        └┘        └┘       └┘                └───┘
par        └─────┘     └┘ └┘  └──┘  └──┘        └┘        └┘       └┘                └───┘
pid                   └┘ └┘  └──┘    └┘        └┘        └┘       └┘                    
st   ─────┘└───────────────────────┘└────────────┘└────────┘└───────┘└──────────────┘└──────┘└┘
 66      { refine ⟨z, hd * r, is_submonoid.mul_mem (monoid.subset_closure hs) hr, _⟩,
id                   └┘     └──────────────────┘  └───────────────────┘ └┘  └┘
src        └─────┘  └┘    └┘└──────────────────┘ └───────────────────┘  └┘  └──┘
typ        └─────┘ └┘└┘ └┘└──────────────────┘ └───────────────────┘└┘└┘└┘└──┘
doc        └─────┘  └┘    └┘                     └───────────────────┘  └┘  └──┘
txt        └─────┘  └┘    └┘                                            └┘  └──┘
par        └─────┘  └┘    └┘                                            └┘  └──┘
pid                └┘    └┘                                            └┘  └──┘
st   ─────┘└───────────────────────────────────────────────────────────────────────┘└─
 67        rw [smul_def, smul_def, mul_left_comm] },
id             └──────┘  └──────┘  └───────────┘
src        └──┘└──────┘└┘└──────┘└┘└───────────┘└┘
typ        └──┘└──────┘└┘└──────┘└┘└───────────┘└┘
doc        └──┘        └┘        └┘             └┘
txt        └──┘        └┘        └┘             └┘
par        └──┘        └┘        └┘             └┘
pid          └┘        └┘        └┘             
st   ─────────────────┘└────────┘└─────────────┘└┘
 68      { refine ⟨-z, r, hr, _⟩, rw [neg_smul, neg_one_mul] } },
id                     └┘          └──────┘  └─────────┘
src        └─────┘  └┘ └┘  └──┘  └──┘└──────┘└┘└─────────┘└┘
typ        └─────┘ └┘└┘└┘└──┘  └──┘└──────┘└┘└─────────┘└┘
doc        └─────┘   └┘ └┘  └──┘  └──┘        └┘└─────────┘└┘
txt        └─────┘   └┘ └┘  └──┘  └──┘        └┘           └┘
par        └─────┘   └┘ └┘  └──┘  └──┘        └┘           └┘
pid                 └┘ └┘  └──┘    └┘        └┘           
st   ──────────────────────────┘└────────────┘└───────────┘└──┘
 69    exact span_le.2 (show monoid.closure s ⊆ adjoin R s, from monoid.closure_subset subset_adjoin)
id           └─────┘         └────────────┘    └────┘         └───────────────────┘ └───────────┘
src    └────┘└─────┘└─┘     └────────────┘ └────┘  └─────┘└───────────────────┘└───────────┘└┘
typ    └────┘└─────┘└─┘     └────────────┘ └────┘└─────┘└───────────────────┘└───────────┘└┘
doc    └────┘       └─┘     └────────────┘          └─────┘└───────────────────┘             └┘
txt    └────┘       └─┘                             └─────┘                                  └┘
par    └────┘       └─┘                             └─────┘                                  └┘
pid                └─┘                             └─────┘                                  
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘
 70  end
st   └─┘
 71  
 72  theorem adjoin_eq_range [decidable_eq R] [decidable_eq A] :
id                            └──────────┘    └──────────┘ 
src                           └──────────┘     └──────────┘
typ                           └──────────┘    └──────────┘ 
 73    adjoin R s = (mv_polynomial.aeval R A s).range :=
id     └────┘     └─────────────────┘    └───┘
src    └────┘       └─────────────────┘       └───┘
typ    └────┘     └─────────────────┘    └───┘
doc                  └─────────────────┘
 74  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 75    (adjoin_le $ λ x hx, ⟨mv_polynomial.X ⟨x, hx⟩, mv_polynomial.eval₂_X _ _ _⟩)
id      └───────┘      └┘   └─────────────┘    └┘   └───────────────────┘
src     └───────┘            └─────────────┘          └───────────────────┘
typ     └───────┘      └┘   └─────────────┘    └┘   └───────────────────┘
doc                          └─────────────┘
 76    (λ x ⟨p, hp⟩, hp ▸ mv_polynomial.induction_on p
id           └┘       └────────────────────────┘
src                      └────────────────────────┘
typ          └┘       └────────────────────────┘
 77      (λ r, by rw [mv_polynomial.aeval_def, mv_polynomial.eval₂_C]; exact (adjoin R s).3 ⟨r, rfl⟩)
id                   └─────────────────────┘  └───────────────────┘          └────┘         └─┘
src               └──┘└─────────────────────┘└┘└───────────────────┘  └────┘ └────┘  └──┘  └┘└─┘
typ              └──┘└─────────────────────┘└┘└───────────────────┘  └────┘ └────┘└──┘ └┘└─┘
doc               └──┘                       └┘                       └────┘         └──┘  └┘   
txt               └──┘                       └┘                       └────┘         └──┘  └┘   
par               └──┘                       └┘                       └────┘         └──┘  └┘   
pid                 └┘                       └┘                                     └──┘  └┘   
st               └──────────────────────────┘└─────────────────────┘└─────────────────────────────┘
 78      (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
id            └┘ └┘        └─────────────┘        └──────────────────────┘ └┘ └┘
src                       └─┘└─────────────┘  └────┘└──────────────────────┘  
typ           └┘ └┘     └─┘└─────────────┘  └────┘└──────────────────────┘└┘└┘
doc                       └─┘                 └────┘                          
txt                       └─┘                 └────┘                          
par                       └─┘                 └────┘                          
pid                                                                         
st                       └───────────────────────────────────────────────────────┘
 79      (λ p ⟨n, hn⟩ hp, by rw [alg_hom.map_mul, mv_polynomial.aeval_def _ _ _ (mv_polynomial.X _),
id                  └┘         └─────────────┘  └─────────────────────┘        └─────────────┘
src                          └──┘└─────────────┘└┘└─────────────────────┘└─────┘ └─────────────┘└────
typ                 └┘     └──┘└─────────────┘└┘└─────────────────────┘└─────┘ └─────────────┘└────
doc                          └──┘               └┘                       └─────┘ └─────────────┘└────
txt                          └──┘               └┘                       └─────┘                └────
par                          └──┘               └┘                       └─────┘                └────
pid                            └┘               └┘                       └─────┘                └────
st                          └──────────────────┘└─────────────────────────────────────────────────┘└─
 80        mv_polynomial.eval₂_X]; exact is_submonoid.mul_mem hp (subset_adjoin hn)))
id         └───────────────────┘         └──────────────────┘ └┘  └───────────┘ └┘
src  ─────┘└───────────────────┘  └────┘└──────────────────┘   └───────────┘  
typ  ─────┘└───────────────────┘  └────┘└──────────────────┘└┘ └───────────┘└┘
doc  ─────┘                       └────┘                                      
txt  ─────┘                       └────┘                                      
par  ─────┘                       └────┘                                      
pid  ─────┘                                                                  
st   ──────────────────────────┘└────────────────────────────────────────────────┘
 81  
 82  theorem adjoin_singleton_eq_range [decidable_eq R] [decidable_eq A] (x : A) :
id                                      └──────────┘    └──────────┘        
src                                     └──────────┘     └──────────┘
typ                                     └──────────┘    └──────────┘        
 83    adjoin R {x} = (polynomial.aeval R A x).range :=
id     └────┘      └──────────────┘    └───┘
src    └────┘        └──────────────┘       └───┘
typ    └────┘      └──────────────┘    └───┘
doc                    └──────────────┘
 84  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 85    (adjoin_le $ set.singleton_subset_iff.2 ⟨polynomial.X, polynomial.eval₂_X _ _⟩)
id      └───────┘   └──────────────────────┘   └──────────┘  └────────────────┘
src     └───────┘   └──────────────────────┘   └──────────┘  └────────────────┘
typ     └───────┘   └──────────────────────┘   └──────────┘  └────────────────┘
doc                                             └──────────┘
 86    (λ y ⟨p, hp⟩, hp ▸ polynomial.induction_on p
id           └┘       └─────────────────────┘
src                      └─────────────────────┘
typ          └┘       └─────────────────────┘
 87      (λ r, by rw [polynomial.aeval_def, polynomial.eval₂_C]; exact (adjoin R _).3 ⟨r, rfl⟩)
id                   └──────────────────┘  └────────────────┘          └────┘          └─┘
src               └──┘└──────────────────┘└┘└────────────────┘  └────┘ └────┘ └────┘  └┘└─┘
typ              └──┘└──────────────────┘└┘└────────────────┘  └────┘ └────┘└────┘ └┘└─┘
doc               └──┘                    └┘                    └────┘        └────┘  └┘   
txt               └──┘                    └┘                    └────┘        └────┘  └┘   
par               └──┘                    └┘                    └────┘        └────┘  └┘   
pid                 └┘                    └┘                                 └────┘  └┘   
st               └───────────────────────┘└──────────────────┘└─────────────────────────────┘
 88      (λ p q hp hq, by rw alg_hom.map_add; exact is_add_submonoid.add_mem hp hq)
id            └┘ └┘        └─────────────┘        └──────────────────────┘ └┘ └┘
src                       └─┘└─────────────┘  └────┘└──────────────────────┘  
typ           └┘ └┘     └─┘└─────────────┘  └────┘└──────────────────────┘└┘└┘
doc                       └─┘                 └────┘                          
txt                       └─┘                 └────┘                          
par                       └─┘                 └────┘                          
pid                                                                         
st                       └───────────────────────────────────────────────────────┘
 89      (λ n r ih, by rw [pow_succ', ← ring.mul_assoc, alg_hom.map_mul, polynomial.aeval_def _ _ _ polynomial.X,
id            └┘         └───────┘    └────────────┘  └─────────────┘  └──────────────────┘       └──────────┘
src                    └──┘└───────┘└──┘└────────────┘└┘└─────────────┘└┘└──────────────────┘└─────┘└──────────┘└─
typ           └┘     └──┘└───────┘└──┘└────────────┘└┘└─────────────┘└┘└──────────────────┘└─────┘└──────────┘└─
doc                    └──┘         └──┘              └┘               └┘                    └─────┘└──────────┘└─
txt                    └──┘         └──┘              └┘               └┘                    └─────┘            └─
par                    └──┘         └──┘              └┘               └┘                    └─────┘            └─
pid                      └┘         └──┘              └┘               └┘                    └─────┘            └─
st                    └────────────┘└────────────────┘└───────────────┘└───────────────────────────────────────┘└─
 90        polynomial.eval₂_X]; exact is_submonoid.mul_mem ih (subset_adjoin $ or.inl rfl)))
id         └────────────────┘         └──────────────────┘ └┘  └───────────┘   └────┘ └─┘
src  ─────┘└────────────────┘  └────┘└──────────────────┘   └───────────┘ └────┘└─┘
typ  ─────┘└────────────────┘  └────┘└──────────────────┘└┘ └───────────┘ └────┘└─┘
doc  ─────┘                    └────┘                                              
txt  ─────┘                    └────┘                                              
par  ─────┘                    └────┘                                              
pid  ─────┘                                                                       
st   ───────────────────────┘└──────────────────────────────────────────────────────────┘
 91  
 92  theorem adjoin_union_coe_submodule : (adjoin R (s ∪ t) : submodule R A) =
id                                         └────┘         └───────┘    
src                                        └────┘            └───────┘      
typ                                        └────┘         └───────┘    
doc                                                           └───────┘
 93    (adjoin R s) * (adjoin R t) :=
id      └────┘      └────┘  
src     └────┘        └────┘
typ     └────┘      └────┘  
 94  begin
st   └─────
 95    rw [adjoin_eq_span, adjoin_eq_span, adjoin_eq_span, span_mul_span],
id         └────────────┘  └────────────┘  └────────────┘  └───────────┘
src    └──┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────────┘
typ    └──┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────────┘
doc    └──┘              └┘              └┘              └┘             
txt    └──┘              └┘              └┘              └┘             
par    └──┘              └┘              └┘              └┘             
pid      └┘              └┘              └┘              └┘             
st   ───────────────────┘└──────────────┘└──────────────┘└─────────────┘└──
 96    congr' 1,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          
st   ─────────┘└─
 97    ext z,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
 98    rw monoid.mem_closure_union_iff,
id        └──────────────────────────┘
src    └─┘└──────────────────────────┘
typ    └─┘└──────────────────────────┘
doc    └─┘└──────────────────────────┘
txt    └─┘
par    └─┘
pid      
st   ────────────────────────────────┘└─
 99    split;
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ─────────
100    { rintro ⟨y, hys, z, hzt, rfl⟩, exact ⟨_, hys, _, hzt, rfl⟩ }
id                                               └─┘     └─┘  └─┘
src      └──────────────────────────┘  └────┘ └─┘   └───┘   └┘└─┘└┘
typ      └──────────────────────────┘  └────┘ └─┘└─┘└───┘└─┘└┘└─┘└┘
doc      └──────────────────────────┘  └────┘ └─┘   └───┘   └┘   └┘
txt      └──────────────────────────┘  └────┘ └─┘   └───┘   └┘   └┘
par      └──────────────────────────┘  └────┘ └─┘   └───┘   └┘   └┘
pid            └────────────────────┘        └─┘   └───┘   └┘   
st   ─┘└────────────────────────────┘└────────────────────────────┘└─
101  end
st   ──┘
102  variables {R s t}
103  
104  theorem adjoin_int (s : set R) : adjoin ℤ s = subalgebra_of_subring (ring.closure s) :=
id                           └─┘     └────┘    └───────────────────┘  └──────────┘ 
src                          └─┘      └────┘     └───────────────────┘  └──────────┘
typ                          └─┘     └────┘    └───────────────────┘  └──────────┘ 
doc                                                └───────────────────┘
st                                  
105  le_antisymm (adjoin_le subset_closure) (closure_subset subset_adjoin)
id   └─────────┘  └───────┘ └────────────┘   └────────────┘ └───────────┘
src  └─────────┘  └───────┘ └────────────┘   └────────────┘ └───────────┘
typ  └─────────┘  └───────┘ └────────────┘   └────────────┘ └───────────┘
106  
107  local attribute [instance] set.pointwise_mul_semiring
id                              └────────────────────────┘
src                             └────────────────────────┘
typ                             └────────────────────────┘
108  
109  theorem fg_trans (h1 : (adjoin R s : submodule R A).fg)
id                           └────┘     └───────┘   └┘
src                          └────┘       └───────┘     └┘
typ                          └────┘     └───────┘   └┘
doc                                       └───────┘
110    (h2 : (adjoin (adjoin R s) t : submodule (adjoin R s) A).fg) :
id            └────┘  └────┘       └───────┘  └────┘     └┘
src           └────┘  └────┘          └───────┘  └────┘        └┘
typ           └────┘  └────┘       └───────┘  └────┘     └┘
doc                                   └───────┘
111    (adjoin R (s ∪ t) : submodule R A).fg :=
id      └────┘         └───────┘   └┘
src     └────┘            └───────┘     └┘
typ     └────┘         └───────┘   └┘
doc                        └───────┘
112  begin
st   └─────
113    rcases fg_def.1 h1 with ⟨p, hp, hp'⟩,
id            └────┘   └┘
src    └─────┘└────┘└─┘  └────────────────┘
typ    └─────┘└────┘└─┘└┘└────────────────┘
doc    └─────┘      └─┘  └────────────────┘
txt    └─────┘      └─┘  └────────────────┘
par    └─────┘      └─┘  └────────────────┘
pid                └─┘  └────────────────┘
st   ─────────────────────────────────────┘└─
114    rcases fg_def.1 h2 with ⟨q, hq, hq'⟩,
id            └────┘   └┘
src    └─────┘└────┘└─┘  └────────────────┘
typ    └─────┘└────┘└─┘└┘└────────────────┘
doc    └─────┘      └─┘  └────────────────┘
txt    └─────┘      └─┘  └────────────────┘
par    └─────┘      └─┘  └────────────────┘
pid                └─┘  └────────────────┘
st   ─────────────────────────────────────┘└─
115    refine fg_def.2 ⟨p * q, set.pointwise_mul_finite hp hq, le_antisymm _ _⟩,
id            └────┘        └──────────────────────┘ └┘ └┘  └─────────┘
src    └─────┘└────┘└─┘   └┘└──────────────────────┘    └┘└─────────┘└───┘
typ    └─────┘└────┘└─┘ └┘└──────────────────────┘└┘└┘└┘└─────────┘└───┘
doc    └─────┘      └─┘    └┘                            └┘           └───┘
txt    └─────┘      └─┘    └┘                            └┘           └───┘
par    └─────┘      └─┘    └┘                            └┘           └───┘
pid                └─┘    └┘                            └┘           └───┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
116    { rw [span_le],
id           └─────┘
src      └──┘└─────┘
typ      └──┘└─────┘
doc      └──┘       
txt      └──┘       
par      └──┘       
pid        └┘       
st   ───┘└─────────┘└──
117      rintros _ ⟨x, hx, y, hy, rfl⟩,
src      └───────────────────────────┘
typ      └───────────────────────────┘
doc      └───────────────────────────┘
txt      └───────────────────────────┘
par      └───────────────────────────┘
pid             └────────────────────┘
st   ────────────────────────────────┘└─
118      change x * y ∈ _,
id                  
src      └─────┘   └┘
typ      └─────┘ └┘
doc      └─────┘    └┘
txt      └─────┘    └┘
par      └─────┘    └┘
pid                └┘
st   ───────────────────┘└─
119      refine is_submonoid.mul_mem _ _,
id              └──────────────────┘
src      └─────┘└──────────────────┘└──┘
typ      └─────┘└──────────────────┘└──┘
doc      └─────┘                    └──┘
txt      └─────┘                    └──┘
par      └─────┘                    └──┘
pid                                └──┘
st   ──────────────────────────────────┘└─
120      { have : x ∈ (adjoin R s : submodule R A),
id                    └────┘     └───────┘   
src        └─────┘   └────┘  └─┘└───────┘  
typ        └─────┘  └────┘└─┘└───────┘ 
doc        └─────┘           └─┘└───────┘  
txt        └─────┘           └─┘           
par        └─────┘           └─┘           
pid        └───┘└┘           └─┘           
st   ─────┘└─────────────────────────────────────┘└─
121        { rw ← hp', exact subset_span hx },
id                └─┘        └─────────┘ └┘
src          └───┘     └────┘└─────────┘  
typ          └───┘└─┘  └────┘└─────────┘└┘
doc          └───┘     └────┘             
txt          └───┘     └────┘             
par          └───┘     └────┘             
pid            └─┘                       
st   ───────┘└──────┘└─────────────────────┘└┘
122        exact adjoin_mono (set.subset_union_left _ _) this },
id               └─────────┘  └───────────────────┘      └──┘
src        └────┘└─────────┘ └───────────────────┘└────┘    
typ        └────┘└─────────┘ └───────────────────┘└────┘└──┘
doc        └────┘                                 └────┘    
txt        └────┘                                 └────┘    
par        └────┘                                 └────┘    
pid                                              └────┘    
st   ────────────────────────────────────────────────────────┘└┘
123      have : y ∈ (adjoin (adjoin R s) t : submodule (adjoin R s) A),
id                          └────┘       └───────┘              
src      └─────┘          └────┘  └┘ └─┘└───────┘         └┘ 
typ      └─────┘         └────┘└┘└─┘└───────┘         └┘
doc      └─────┘                  └┘ └─┘└───────┘         └┘ 
txt      └─────┘                  └┘ └─┘                  └┘ 
par      └─────┘                  └┘ └─┘                  └┘ 
pid      └───┘└┘                  └┘ └─┘                  └┘ 
st   ────────────────────────────────────────────────────────────────┘└─
124      { rw ← hq', exact subset_span hy },
id              └─┘        └─────────┘ └┘
src        └───┘     └────┘└─────────┘  
typ        └───┘└─┘  └────┘└─────────┘└┘
doc        └───┘     └────┘             
txt        └───┘     └────┘             
par        └───┘     └────┘             
pid          └─┘                       
st   ────┘ └──────┘└─────────────────────┘ 
125      change y ∈ adjoin R (s ∪ t), rwa adjoin_union },
id                 └────┘     
src      └─────┘  └────┘    
typ      └─────┘ └────┘ 
doc      └─────┘             
txt      └─────┘             
par      └─────┘             
pid                         
st   ──────────────────────────────┘                   
126    { intros r hr,
127      change r ∈ adjoin R (s ∪ t) at hr,
128      rw adjoin_union at hr,
129      change r ∈ (adjoin (adjoin R s) t : submodule (adjoin R s) A) at hr,
130      haveI := classical.dec_eq A,
131      haveI := classical.dec_eq R,
132      rw [← hq', ← set.image_id q, finsupp.mem_span_iff_total (adjoin R s)] at hr,
133      rcases hr with ⟨l, hlq, rfl⟩,
134      have := @finsupp.total_apply A A (adjoin R s),
135      rw [this, finsupp.sum, mem_coe],
136      refine sum_mem _ _,
137      intros z hz, change (l z).1 * _ ∈ _,
138      have : (l z).1 ∈ (adjoin R s : submodule R A) := (l z).2,
139      rw [← hp', ← set.image_id p, finsupp.mem_span_iff_total R] at this,
140      rcases this with ⟨l2, hlp, hl⟩,
141      have := @finsupp.total_apply A A R,
142      rw this at hl,
143      rw [←hl, finsupp.sum_mul],
144      refine sum_mem _ _,
145      intros t ht, change _ * _ ∈ _, rw smul_mul_assoc, refine smul_mem _ _ _,
146      exact subset_span ⟨t, hlp ht, z, hlq hz, rfl⟩ }
st                                                     └─
147  end
st   ──┘
148  
149  end algebra
150  
151  namespace subalgebra
152  
153  variables {R : Type u} {A : Type v}
154  variables [comm_ring R] [comm_ring A] [algebra R A]
id              └───────┘     └───────┘     └─────┘
src             └───────┘     └───────┘     └─────┘
typ             └───────┘     └───────┘     └─────┘
doc                                         └─────┘
155  
156  def fg (S : subalgebra R A) : Prop :=
id               └────────┘  
src              └────────┘
typ              └────────┘  
157  ∃ t : finset A, algebra.adjoin R ↑t = S
id        └────┘  └────────────┘    
src       └────┘   └────────────┘     
typ       └────┘  └────────────┘    
doc        └────┘
158  
159  theorem fg_def {S : subalgebra R A} : S.fg ↔ ∃ t : set A, set.finite t ∧ algebra.adjoin R t = S :=
id                       └────────┘      └─┘       └─┘  └────────┘   └────────────┘    
src                      └────────┘         └─┘       └─┘   └────────┘    └────────────┘     
typ                      └────────┘      └─┘       └─┘  └────────┘   └────────────┘    
doc                                                            └────────┘
160  ⟨λ ⟨t, ht⟩, ⟨↑t, set.finite_mem_finset t, ht⟩,
id        └┘       └───────────────────┘
src                  └───────────────────┘
typ       └┘       └───────────────────┘
161  λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa finset.coe_to_finset⟩⟩
id        └─┘            └────────┘         └──────────────────┘
src                       └────────┘     └──┘└──────────────────┘
typ       └─┘            └────────┘     └──┘└──────────────────┘
doc                       └────────┘     └──┘
txt                                      └──┘
par                                      └──┘
pid                                         
st                                      └───────────────────────┘
162  
163  theorem fg_bot : (⊥ : subalgebra R A).fg :=
id                        └────────┘   └┘
src                       └────────┘     └┘
typ                       └────────┘   └┘
164  ⟨∅, algebra.adjoin_empty R A⟩
id      └──────────────────┘  
src     └──────────────────┘
typ     └──────────────────┘  
165  
166  end subalgebra
167  
168  variables {R : Type u} {A : Type v} {B : Type w}
169  variables [comm_ring R] [comm_ring A] [comm_ring B] [algebra R A] [algebra R B]
id              └───────┘     └───────┘     └───────┘     └─────┘       └─────┘
src             └───────┘     └───────┘     └───────┘     └─────┘       └─────┘
typ             └───────┘     └───────┘     └───────┘     └─────┘       └─────┘
doc                                                       └─────┘       └─────┘
170  
171  instance alg_hom.is_noetherian_ring_range (f : A →ₐ[R] B) [is_noetherian_ring A] :
id                                                   └─┘    └────────────────┘ 
src                                                   └─┘      └────────────────┘
typ                                                  └─┘    └────────────────┘ 
doc                                                   └─┘ 
172    is_noetherian_ring f.range :=
id     └────────────────┘ └────┘
src    └────────────────┘  └────┘
typ    └────────────────┘ └────┘
173  is_noetherian_ring_range f
id   └──────────────────────┘ 
src  └──────────────────────┘
typ  └──────────────────────┘ 
174  
175  variables [decidable_eq R] [decidable_eq A]
id              └──────────┘     └──────────┘
src             └──────────┘     └──────────┘
typ             └──────────┘     └──────────┘
176  
177  theorem is_noetherian_ring_of_fg {S : subalgebra R A} (HS : S.fg)
id                                         └────────┘          └─┘
src                                        └────────┘             └─┘
typ                                        └────────┘          └─┘
178    [is_noetherian_ring R] : is_noetherian_ring S :=
id      └────────────────┘     └────────────────┘ 
src     └────────────────┘      └────────────────┘
typ     └────────────────┘     └────────────────┘ 
179  let ⟨t, ht⟩ := HS in ht ▸ (algebra.adjoin_eq_range R (↑t : set A)).symm ▸
id   └─┘    └┘     └┘         └─────────────────────┘       └─┘   └──┘  
src                            └─────────────────────┘        └─┘    └──┘  
typ  └─┘    └┘     └┘         └─────────────────────┘       └─┘   └──┘  
180  by haveI : is_noetherian_ring (mv_polynomial (↑t : set A) R) :=
id              └────────────────┘  └───────────┘     └─┘   
src     └──────┘└────────────────┘ └───────────┘  └─┘└─┘ └┘ └───┘
typ     └──────┘└────────────────┘ └───────────┘ └─┘└─┘└┘└───┘
doc     └──────┘                   └───────────┘   └─┘    └┘ └───┘
txt     └──────┘                                   └─┘    └┘ └───┘
par     └──────┘                                   └─┘    └┘ └───┘
pid          └┘                                   └─┘    └┘ └──┘
st     └─────────────────────────────────────────────────────────────
181  is_noetherian_ring_mv_polynomial_of_fintype;
id   └─────────────────────────────────────────┘
src  └─────────────────────────────────────────┘
typ  └─────────────────────────────────────────┘
st   ─────────────────────────────────────────────
182  convert alg_hom.is_noetherian_ring_range _; apply_instance
id           └──────────────────────────────┘
src  └──────┘└──────────────────────────────┘└┘  └──────────────
typ  └──────┘└──────────────────────────────┘└┘  └──────────────
doc  └──────┘                                └┘  └──────────────
txt  └──────┘                                └┘  └──────────────
par  └──────┘                                └┘  └──────────────
pid                                         └┘                
st   ───────────────────────────────────────────────────────────
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  theorem is_noetherian_ring_closure (s : set R) (hs : s.finite) :
id                                           └─┘         └─────┘
src                                          └─┘           └─────┘
typ                                          └─┘         └─────┘
doc                                                        └─────┘
185    is_noetherian_ring (ring.closure s) :=
id     └────────────────┘  └──────────┘ 
src    └────────────────┘  └──────────┘
typ    └────────────────┘  └──────────┘ 
186  show is_noetherian_ring (subalgebra_of_subring (ring.closure s)), from
id        └────────────────┘  └───────────────────┘  └──────────┘ 
src       └────────────────┘  └───────────────────┘  └──────────┘
typ       └────────────────┘  └───────────────────┘  └──────────┘ 
doc                           └───────────────────┘
187  algebra.adjoin_int s ▸ is_noetherian_ring_of_fg (subalgebra.fg_def.2 ⟨s, hs, rfl⟩)
id   └────────────────┘   └──────────────────────┘  └───────────────┘     └┘  └─┘
src  └────────────────┘    └──────────────────────┘  └───────────────┘          └─┘
typ  └────────────────┘   └──────────────────────┘  └───────────────┘     └┘  └─┘